$\forall$${\it es}$:ES, $A$:Type, $X$, $Y$:AbsInterface($A$).
\\[0ex]($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ $X$)) $\Leftarrow\!\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ $Y$))) $\Rightarrow$ ($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ ($X$($e$) = $Y$($e$) $\in$ $A$)) $\Rightarrow$ ($X$ = $Y$)